<html>
<head><meta charset="utf-8"><title>Can we do without provenance? · t-lang/wg-unsafe-code-guidelines · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/index.html">t-lang/wg-unsafe-code-guidelines</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html">Can we do without provenance?</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="219882255"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219882255" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219882255">(Dec 14 2020 at 18:29)</a>:</h4>
<p>Some more thoughts on <span class="user-mention" data-user-id="271719">@Mario Carneiro</span>'s idea to have provenance "on values" but not "in memory"...</p>
<p>My main concern with that proposal is this: losing provenance is bad news. In Stacked Borrows and everywhere else, if you cast a ptr to an integer, you give up everything you know about that pointer as now anyone might cast that integer back to a ptr, possibly even by "guessing" the integer if you leaked enough information about that. One might call this a "broadcast" operation, since the memory is now available to everyone. So, under a provenance model, a ptr-to-int cast is bad news for the alias analysis.<br>
If memory doesn't remember provenance, <em>every time a ptr is stored in memory is a boradcast</em>. Which is basically all the time since even local variables are backed by memory -- at least the adressable ones.<br>
(And making a distinction between two kinds of local variables seems risky -- there's code that would be UB with one kind of variable but fine with the other, so in the hope of resolving the counterintuitive behavior arising from provenance you have introduced something similarly counterintuitive.)</p>



<a name="219882608"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219882608" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219882608">(Dec 14 2020 at 18:31)</a>:</h4>
<p>What if instead of provenance, you track "permission" to access data? So you are allowed to invent whatever bit pattern you like, but it is UB to read random memory you have magicked up in this way</p>



<a name="219882760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219882760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219882760">(Dec 14 2020 at 18:32)</a>:</h4>
<p>This probably isn't possible in C, but rust's references give a pretty good guide to what permission you should have</p>



<a name="219883059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883059">(Dec 14 2020 at 18:35)</a>:</h4>
<blockquote>
<p>One might call this a "broadcast" operation, since the memory is now available to everyone.</p>
</blockquote>
<p>That is, the bit pattern is available to everyone, but the permission is only yours, and anyone else who tries to access the memory will cause UB.</p>



<a name="219883436"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883436" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883436">(Dec 14 2020 at 18:38)</a>:</h4>
<p>These permissions are tracked "alongside" values, but are not literally stored with values. Logically, we would say that the permission is the points-to assertion while the value is the bit pattern</p>



<a name="219883523"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883523" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883523">(Dec 14 2020 at 18:38)</a>:</h4>
<p>How does this differ from provenance?</p>



<a name="219883746"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883746" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883746">(Dec 14 2020 at 18:40)</a>:</h4>
<p>Mostly that it's not tied so directly to values that it has to get filtered through every operation. It's more similar to the facts that the compiler builds up by looking at flow control</p>



<a name="219883814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883814">(Dec 14 2020 at 18:40)</a>:</h4>
<p>if these permissions only exist in the compiler analysis they don't change anything about the program semantics</p>



<a name="219883826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883826">(Dec 14 2020 at 18:40)</a>:</h4>
<p>that's right</p>



<a name="219883829"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883829" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883829">(Dec 14 2020 at 18:40)</a>:</h4>
<p>as in, they cannot make things UB</p>



<a name="219883852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883852">(Dec 14 2020 at 18:40)</a>:</h4>
<p>if they are involved in UB in any way, this sounds like another form of provenance to me</p>



<a name="219883901"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219883901" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219883901">(Dec 14 2020 at 18:41)</a>:</h4>
<p>there are hardware architectures like CHERI where pointers carry something like permissions, and I'd call that a form of provenance</p>



<a name="219884206"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884206" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884206">(Dec 14 2020 at 18:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219883436">said</a>:</p>
<blockquote>
<p>These permissions are tracked "alongside" values, but are not literally stored with values. Logically, we would say that the permission is the points-to assertion while the value is the bit pattern</p>
</blockquote>
<p>points-to assertions only exist in the logic, so they cannot actually help make things UB and thus enable optimizations.<br>
unless you want to say that the compiler contract becomes something like "code is UB unless you can prove a separation logic spec about it"... at which point you've replaced provenance by something that I don't think has a name but might be called PROVENANCE since there's just <em>so much</em> "extra state" now.^^ also you made your language semantics uncomputable. I don't think I'm a fan of this approach.^^</p>



<a name="219884457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884457">(Dec 14 2020 at 18:45)</a>:</h4>
<p>I suppose in that respect they are like provenance. I have some operations that allow you to literally separate the pointer from the permission and compute with the latter, but I'm afraid it is actually the programmer doing separation logic in disguise</p>



<a name="219884528"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884528" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884528">(Dec 14 2020 at 18:45)</a>:</h4>
<p>not to mention there's a cyclicity now -- the separation logic will be defined in terms of the operational semantics of the language (or at least related to it in its adequacy/soundness statement), and now the op.sem depends on the logic.</p>



<a name="219884635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884635">(Dec 14 2020 at 18:46)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219884457">said</a>:</p>
<blockquote>
<p>I suppose in that respect they are like provenance. I have some operations that allow you to literally separate the pointer from the permission and compute with the latter, but I'm afraid it is actually the programmer doing separation logic in disguise</p>
</blockquote>
<p>even in C/LLVM/Rust-style provenance you could imagine adding operations that allow the programmer to handle provenance more explicitly</p>



<a name="219884719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884719">(Dec 14 2020 at 18:47)</a>:</h4>
<p>in fact people have already written functions like</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="sd">/// Returns a pointer with the provenance of `prov` pointing to `addr`.</span>
<span class="k">fn</span> <span class="nf">copy_provenance</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">addr</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">,</span><span class="w"> </span><span class="n">prov</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="w"></span>
</code></pre></div>



<a name="219884895"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884895" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884895">(Dec 14 2020 at 18:48)</a>:</h4>
<p>The part where C/LLVM-style provenance starts to get weird for me is when it gets sliced and diced and sent over the network though</p>



<a name="219884919"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884919" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884919">(Dec 14 2020 at 18:48)</a>:</h4>
<p>but so far there's little work on this and indeed it could be interesting to work out what a set of useful primitives for "working with provenance" could be.</p>



<a name="219884931"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884931" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884931">(Dec 14 2020 at 18:48)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219884895">said</a>:</p>
<blockquote>
<p>The part where provenance starts to get weird for me is when it gets sliced and diced and sent over the network though</p>
</blockquote>
<p>yeah, you can't do that^^</p>



<a name="219884942"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219884942" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219884942">(Dec 14 2020 at 18:48)</a>:</h4>
<p>there's always ptr-int casts and back</p>



<a name="219885092"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219885092" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219885092">(Dec 14 2020 at 18:49)</a>:</h4>
<p>From my point of view it's the pointer that gets sliced and diced while the permission just sits there alongside. If you don't smuggle the permission separately then the pointer that comes out the other end is UB to use</p>



<a name="219885393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219885393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219885393">(Dec 14 2020 at 18:51)</a>:</h4>
<p>One can imagine the compiler being able to route the permissions in most cases (similar to value computations with provenance), but for anything like ptr-int casts the programmer needs to be a bit more hands on</p>



<a name="219885840"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219885840" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219885840">(Dec 14 2020 at 18:54)</a>:</h4>
<p>Or I guess, when the programmer is not working in literal separation logic, they just do the op and if the permission isn't derivable from the function inputs then you get UB</p>



<a name="219886003"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886003" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886003">(Dec 14 2020 at 18:56)</a>:</h4>
<p>Regarding op.sem circularity, I don't think it's a problem because you can define the operational semantics with respect only to a flat memory model, and layer language level UB on top of that</p>



<a name="219886049"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886049" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886049">(Dec 14 2020 at 18:56)</a>:</h4>
<p>you can but then you cant exploit that language-level UB in proofs that you perform in the logic</p>



<a name="219886068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886068">(Dec 14 2020 at 18:56)</a>:</h4>
<p>since the logic is used to define language-level UB in the first place</p>



<a name="219886095"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886095" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886095">(Dec 14 2020 at 18:56)</a>:</h4>
<p>so, that seems like a problem. maybe it isn't, but my intuition says it is.</p>



<a name="219886102"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886102" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886102">(Dec 14 2020 at 18:57)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219885393">said</a>:</p>
<blockquote>
<p>One can imagine the compiler being able to route the permissions in most cases (similar to value computations with provenance), but for anything like ptr-int casts the programmer needs to be a bit more hands on</p>
</blockquote>
<p>the compiler doesn't have to route anything, this is an abstract machine concept we are talking about.</p>



<a name="219886655"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886655" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886655">(Dec 14 2020 at 19:00)</a>:</h4>
<p>ah right, that's the problem with UB style formalization: since it's a negative property, you can't have a gap between what the compiler can reason about and what is language UB. If the compiler is allowed to say no even on some programs with no UB then you have some more flexibility</p>



<a name="219886762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219886762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219886762">(Dec 14 2020 at 19:01)</a>:</h4>
<p>i.e. the compiler says "I was not able to ensure this program has no UB, please add assertions here and there and then I will think about compiling your code"</p>



<a name="219887012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219887012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219887012">(Dec 14 2020 at 19:03)</a>:</h4>
<p>and the assertions are what actually change the operational semantics and introduce the necessary UB</p>



<a name="219889012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219889012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219889012">(Dec 14 2020 at 19:19)</a>:</h4>
<p>but that's all ivory tower stuff again</p>



<a name="219892177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219892177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219892177">(Dec 14 2020 at 19:40)</a>:</h4>
<p>Cranelift by default doesn't optimize memory operations. It does have a way to explicitly assert that loads/stores are aligned, don't trap or for loads that the loaded memory is constant during the execution of the current function though. While this is slightly different from your proposal (assume no UB vs erroring when absence of UB couldn't be proved) either way you have to explicitly add UB to your program.</p>



<a name="219901749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219901749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219901749">(Dec 14 2020 at 21:04)</a>:</h4>
<p>I don't think that has anything to do with UB being negative</p>



<a name="219901764"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219901764" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219901764">(Dec 14 2020 at 21:04)</a>:</h4>
<p>taking a negation doesn't change anything about the cyclicity^^</p>



<a name="219901975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219901975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219901975">(Dec 14 2020 at 21:06)</a>:</h4>
<p>btw, one thing I am still wondering about <span class="user-mention" data-user-id="271719">@Mario Carneiro</span> -- which of the three optimizations do you want to drop? it's one thing to say "memory shouldnt have provenance", but you'll still need to pick 2 (or fewer) out of 3 optimizations that you can make valid in this model. this is a fundamental choice each model will have to make (and we can categorize the models in 3 groups using this)</p>



<a name="219902340"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219902340" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219902340">(Dec 14 2020 at 21:09)</a>:</h4>
<p>I think this framing is begging the question a bit, but to first approximation I would say the third one would be rejected because the reasoning that was used to get the first optimization would retain enough information to not make it look like q was never written to in the third optimization</p>



<a name="219911475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219911475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219911475">(Dec 14 2020 at 22:28)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219884719">said</a>:</p>
<blockquote>
<p>in fact people have already written functions like</p>
<p><div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="sd">/// Returns a pointer with the provenance of `prov` pointing to `addr`.</span>
<span class="k">fn</span> <span class="nf">copy_provenance</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">addr</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">,</span><span class="w"> </span><span class="n">prov</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="w"></span>
</code></pre></div><br>
</p>
</blockquote>
<p>How do you write that function without offsetting from one pointer into a different allocation?</p>



<a name="219911923"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219911923" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219911923">(Dec 14 2020 at 22:32)</a>:</h4>
<p>You wouldn't, but using <code>.wrapping_offset</code> is defined for that.</p>



<a name="219912142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219912142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219912142">(Dec 14 2020 at 22:34)</a>:</h4>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">fn</span> <span class="nf">copy_provenance</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">addr</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">,</span><span class="n">prov</span>: <span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">)</span>-&gt;<span class="o">*</span><span class="k">mut</span><span class="w"> </span><span class="n">T</span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">prov</span><span class="p">.</span><span class="n">wrapping_offset</span><span class="p">((</span><span class="n">prov</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="kt">usize</span><span class="w"> </span><span class="o">-</span><span class="w"> </span><span class="n">addr</span><span class="w"> </span><span class="k">as</span><span class="w"> </span><span class="kt">usize</span><span class="p">)</span><span class="o">/</span><span class="n">mem</span>::<span class="n">size_of</span>::<span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">());</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>Would be a definition of that (which notably does not use any unsafe)</p>



<a name="219912271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219912271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219912271">(Dec 14 2020 at 22:35)</a>:</h4>
<p>In a world where provenance exists, how is that pointer usable?</p>



<a name="219912363"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219912363" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219912363">(Dec 14 2020 at 22:36)</a>:</h4>
<p>It would be useable iff addr points within the provenance of prov.</p>



<a name="219912546"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219912546" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219912546">(Dec 14 2020 at 22:38)</a>:</h4>
<p>(there we go. Don't mind me failing to write rust properly)</p>



<a name="219912673"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219912673" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219912673">(Dec 14 2020 at 22:39)</a>:</h4>
<p>Perhaps prov is from <code>sl.as_ptr()</code>, and addr is <code>&amp;mut sl[0] as *mut T</code>, where <code>sl</code> has type <code>&amp;mut [T]</code></p>



<a name="219913043"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219913043" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219913043">(Dec 14 2020 at 22:43)</a>:</h4>
<p><span class="user-mention silent" data-user-id="257758">Connor Horman</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219912673">said</a>:</p>
<blockquote>
<p>Perhaps prov is from <code>sl.as_ptr()</code>, and addr is <code>&amp;mut sl[0] as *mut T</code>, where <code>sl</code> has type <code>&amp;mut [T]</code></p>
</blockquote>
<p>Do those not have the same provenance? They come from the same allocation.</p>



<a name="219913068"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219913068" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Josh Triplett <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219913068">(Dec 14 2020 at 22:43)</a>:</h4>
<p>Or am I misunderstanding something?</p>



<a name="219913388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219913388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> simulacrum <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219913388">(Dec 14 2020 at 22:46)</a>:</h4>
<p>No, one only has "access" to the first element of the slice whereas as_ptr gives you access to the whole slice (at least by my understanding)</p>



<a name="219913685"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219913685" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Connor Horman <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219913685">(Dec 14 2020 at 22:49)</a>:</h4>
<p>Indeed, under a strict interpretation of stacked borrows.</p>



<a name="219956167"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219956167" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219956167">(Dec 15 2020 at 09:51)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219902340">said</a>:</p>
<blockquote>
<p>I think this framing is begging the question a bit, but to first approximation I would say the third one would be rejected because the reasoning that was used to get the first optimization would retain enough information to not make it look like q was never written to in the third optimization</p>
</blockquote>
<p>I dont think this is begging any question, these are just three transformations and for each of them an abstract machine def.n has to answer "is this correct, yes or no". that's the point of having a precise def.n.</p>
<p>I meant the first optimization <em>exactly as shown</em>, not some variant of the optimization that adds anything extra to "preserve something". that's a different optimization. once you start changing the optimizations, it's easy to make all three of them correct.</p>



<a name="219956229"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219956229" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219956229">(Dec 15 2020 at 09:51)</a>:</h4>
<p><span class="user-mention silent" data-user-id="239881">Josh Triplett</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219913043">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="257758">Connor Horman</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219912673">said</a>:</p>
<blockquote>
<p>Perhaps prov is from <code>sl.as_ptr()</code>, and addr is <code>&amp;mut sl[0] as *mut T</code>, where <code>sl</code> has type <code>&amp;mut [T]</code></p>
</blockquote>
<p>Do those not have the same provenance? They come from the same allocation.</p>
</blockquote>
<p>they have the same provenance is C, but not in Stacked Borrows</p>



<a name="219956393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219956393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219956393">(Dec 15 2020 at 09:53)</a>:</h4>
<blockquote>
<p>I meant the first optimization exactly as shown, not some variant of the optimization that adds anything extra to "preserve something".</p>
</blockquote>
<p>The problem with "exactly as shown" in your examples in the blog post is that they are written in C and two of those programs would be UB in C</p>



<a name="219956522"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219956522" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219956522">(Dec 15 2020 at 09:54)</a>:</h4>
<p>I charitably interpret the optimizations to be working on some IR, and on that IR I'm saying there would be operations introduced in the first optimization, not shown in the example because they aren't representable in C anyway, that would block the third optimization</p>



<a name="219957255"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957255" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957255">(Dec 15 2020 at 10:01)</a>:</h4>
<p>Put more precisely, the way I resolve the issue with GVN style optimizations that transform <code>if p == q { f(p) }</code> to <code>if p == q { f(q) }</code> is that at the source level these are not equivalent because they have different inferred preconditions even though they are the same operation. That is, the first one elaborates to IR that looks like</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">if</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">   </span><span class="n">assert</span><span class="p">(</span><span class="n">p</span><span class="w"> </span><span class="n">is</span><span class="w"> </span><span class="n">usable</span><span class="w"> </span><span class="n">here</span><span class="p">);</span><span class="w"></span>
<span class="w">   </span><span class="n">f</span><span class="p">(</span><span class="n">p</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>and GVN can rewrite this to</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">if</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">   </span><span class="n">assert</span><span class="p">(</span><span class="n">p</span><span class="w"> </span><span class="n">is</span><span class="w"> </span><span class="n">usable</span><span class="w"> </span><span class="n">here</span><span class="p">);</span><span class="w"></span>
<span class="w">   </span><span class="n">f</span><span class="p">(</span><span class="n">q</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>or perhaps</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">if</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">   </span><span class="n">assert</span><span class="p">(</span><span class="n">q</span><span class="w"> </span><span class="n">is</span><span class="w"> </span><span class="n">usable</span><span class="w"> </span><span class="n">here</span><span class="w"> </span><span class="n">via</span><span class="w"> </span><span class="n">an</span><span class="w"> </span><span class="n">equality</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">q</span><span class="p">);</span><span class="w"></span>
<span class="w">   </span><span class="n">f</span><span class="p">(</span><span class="n">q</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>but this is not the same as the result of the rewritten source program <code>if p == q { f(q) }</code>, which obtains:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">if</span><span class="w"> </span><span class="n">p</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="n">q</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">   </span><span class="n">assert</span><span class="p">(</span><span class="n">q</span><span class="w"> </span><span class="n">is</span><span class="w"> </span><span class="n">usable</span><span class="w"> </span><span class="n">here</span><span class="p">);</span><span class="w"></span>
<span class="w">   </span><span class="n">f</span><span class="p">(</span><span class="n">q</span><span class="p">)</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>It is possible for this version to be UB while the first two are not.</p>



<a name="219957333"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957333" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957333">(Dec 15 2020 at 10:02)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219956393">said</a>:</p>
<blockquote>
<blockquote>
<p>I meant the first optimization exactly as shown, not some variant of the optimization that adds anything extra to "preserve something".</p>
</blockquote>
<p>The problem with "exactly as shown" in your examples in the blog post is that they are written in C and two of those programs would be UB in C</p>
</blockquote>
<p>they are written in LLVM IR using C syntax</p>



<a name="219957356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957356">(Dec 15 2020 at 10:02)</a>:</h4>
<p>I assume that syntax has equivalences in whatever language you are imagining</p>



<a name="219957388"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957388" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957388">(Dec 15 2020 at 10:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219956522">said</a>:</p>
<blockquote>
<p>I charitably interpret the optimizations to be working on some IR, and on that IR I'm saying there would be operations introduced in the first optimization, not shown in the example because they aren't representable in C anyway, that would block the third optimization</p>
</blockquote>
<p>that's a different optimization. I explicitly mean the syntax to reflect everything that happens.</p>



<a name="219957433"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957433" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957433">(Dec 15 2020 at 10:03)</a>:</h4>
<p>if the IR has extra operations, it's easy to make up some syntax to represent them.</p>



<a name="219957523"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957523" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957523">(Dec 15 2020 at 10:04)</a>:</h4>
<p>I don't disagree that LLVM, with its current set of optimizations and representation for these concepts, is in a bind</p>



<a name="219957551"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957551" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957551">(Dec 15 2020 at 10:04)</a>:</h4>
<p>okay so what you are saying later seems to be that the first optimization is not correct, i.e., integers have provenance <span aria-label="scared" class="emoji emoji-1f628" role="img" title="scared">:scared:</span></p>



<a name="219957605"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957605" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957605">(Dec 15 2020 at 10:04)</a>:</h4>
<p>because if integers did not have provenance, then any predicate holding for <code>p: uintptr_t</code> also holds for <code>q: uintptr_t</code> after we know that <code>p==q</code></p>



<a name="219957638"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957638" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957638">(Dec 15 2020 at 10:05)</a>:</h4>
<p>In the code snippets just shown, <code>p</code> and <code>q</code> are plain bit patterns</p>



<a name="219957659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957659">(Dec 15 2020 at 10:05)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219957638">said</a>:</p>
<blockquote>
<p>In the code snippets just shown, <code>p</code> and <code>q</code> are plain bit patterns</p>
</blockquote>
<p>that's a contradiction to what you said before :)</p>



<a name="219957664"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957664" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957664">(Dec 15 2020 at 10:05)</a>:</h4>
<p>the provenance is all in the assertions</p>



<a name="219957683"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957683" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957683">(Dec 15 2020 at 10:05)</a>:</h4>
<p>if they are plain bit patterns and <code>p == q</code>, then <code>pred(p)</code> implies <code>pred(q)</code></p>



<a name="219957749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957749">(Dec 15 2020 at 10:06)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219957664">said</a>:</p>
<blockquote>
<p>the provenance is all in the assertions</p>
</blockquote>
<p>I have no idea what that means. either the provenance affects UB, then it exists in the abstract machine, or it doesnt, then it is irrelevant for this discussion.</p>



<a name="219957777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957777">(Dec 15 2020 at 10:06)</a>:</h4>
<p>Well, <code>p is usable here</code> is a more complex thing, that refers to the way that <code>p</code> was obtained in the function, i.e. what you would call provenance</p>



<a name="219957819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957819">(Dec 15 2020 at 10:07)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219957777">said</a>:</p>
<blockquote>
<p>Well, <code>p is usable here</code> is a more complex thing, that refers to the way that <code>p</code> was obtained in the function, i.e. what you would call provenance</p>
</blockquote>
<p>but then integers do have provenance, in the abstract machine</p>



<a name="219957828"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957828" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957828">(Dec 15 2020 at 10:07)</a>:</h4>
<p>which makes e.g. <code>x-x</code> very different from <code>0</code></p>



<a name="219957855"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957855" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957855">(Dec 15 2020 at 10:07)</a>:</h4>
<p>No? Again, <code>p</code> is just a plain number</p>



<a name="219957927"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957927" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957927">(Dec 15 2020 at 10:08)</a>:</h4>
<p>I think you are contradicting yourself, and this is somewhat obfuscated by your approach to a "logic-based model", but once you make that precise the contradiction will show itself plainly</p>



<a name="219957940"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957940" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957940">(Dec 15 2020 at 10:08)</a>:</h4>
<p>but if you rewrite <code>x-x</code> to <code>0</code> you might still have a lingering assertion that makes reference to the way that <code>x</code> was obtained</p>



<a name="219957974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957974">(Dec 15 2020 at 10:09)</a>:</h4>
<p>you cannot at the same time posit "<code>p</code> is just a plain number" and "a predicate on <code>p</code>, like <code>usable(p)</code>, reflects the way that <code>p</code> was computed"</p>



<a name="219957996"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219957996" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219957996">(Dec 15 2020 at 10:09)</a>:</h4>
<p>I just don't think of provenance as attached to values, and your persistence to that POV is making us talk past each other</p>



<a name="219958007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958007">(Dec 15 2020 at 10:09)</a>:</h4>
<p>it's not a predicate on p</p>



<a name="219958012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958012">(Dec 15 2020 at 10:09)</a>:</h4>
<p>or at least not only on p</p>



<a name="219958013"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958013" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958013">(Dec 15 2020 at 10:09)</a>:</h4>
<p>I only insist on formal precision / explicitness</p>



<a name="219958063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958063">(Dec 15 2020 at 10:10)</a>:</h4>
<p>formally it's a points to predicate</p>



<a name="219958113"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958113" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958113">(Dec 15 2020 at 10:10)</a>:</h4>
<p>which gets passed down through the control flow</p>



<a name="219958199"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958199" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958199">(Dec 15 2020 at 10:11)</a>:</h4>
<p>this predicate will involve facts about the parenthood of <code>p</code> even if you rewrite all the <code>p</code>'s to <code>q</code>'s</p>



<a name="219958298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958298">(Dec 15 2020 at 10:12)</a>:</h4>
<p>because the parenthood of <code>p</code> is some set of other local variables in the function, not literally a predicate "the set of all things that <code>p</code> was obtained from"</p>



<a name="219958323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958323">(Dec 15 2020 at 10:12)</a>:</h4>
<p>because that's not something that you can define as a function of the bit pattern that is <code>p</code></p>



<a name="219958395"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958395" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958395">(Dec 15 2020 at 10:13)</a>:</h4>
<p>well... whatever that means.^^<br>
I appreciate that this is just a sketch in your mind and not fully worked out. I encourage you to boil this down to the bare minimum that is still interesting, and try to work it out in more formal detail. define the syntax of your language, define its semantics, define UB, see what makes an optimization "correct".</p>



<a name="219958834"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958834" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958834">(Dec 15 2020 at 10:17)</a>:</h4>
<p>I have a <a href="https://github.com/digama0/mm0/blob/master/mm0-rs/mmc.md">language spec</a>, but it isn't really framed to answer this question, and the compiler isn't done yet so it's hard to demonstrate these details. I will see if I can write something self contained and more coherent</p>



<a name="219958896"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958896" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958896">(Dec 15 2020 at 10:18)</a>:</h4>
<p>To solve a hard problem like this, you actually need to do something <em>fundamentally different</em>, not just have a more complicated syntax and a more complicated notion of UB that involves a logic of some sort. I currently lack the imagination for what that different thing might be, and it hasn't become clear in what you wrote so far. If this works, there must be a <em>key insight</em> that makes it work.</p>



<a name="219958911"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958911" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958911">(Dec 15 2020 at 10:18)</a>:</h4>
<p>An actual compiler is explicitly not required since these are all theoretical discussions ;)</p>



<a name="219958976"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219958976" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219958976">(Dec 15 2020 at 10:19)</a>:</h4>
<p>The <em>fundamental</em> difference in the language I'm working on is that the programmer collaborates with the compiler to make these proofs go through</p>



<a name="219959038"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959038" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959038">(Dec 15 2020 at 10:20)</a>:</h4>
<p>the compiler doesn't just guess all the predicates based on UB ops</p>



<a name="219959055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959055">(Dec 15 2020 at 10:20)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219958834">said</a>:</p>
<blockquote>
<p>I have a <a href="https://github.com/digama0/mm0/blob/master/mm0-rs/mmc.md">language spec</a>, but it isn't really framed to answer this question, and the compiler isn't done yet so it's hard to demonstrate these details. I will see if I can write something self contained and more coherent</p>
</blockquote>
<p>my recommendation would be to boil this down to a bare minimum.  the goal is not to create a usable language, the goal is to break my claim of this being a fundamental tradeoff in language design. a single integer type and a single pointer type are more than enough for that, for example.</p>



<a name="219959125"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959125" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959125">(Dec 15 2020 at 10:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219958976">said</a>:</p>
<blockquote>
<p>The <em>fundamental</em> difference in the language I'm working on is that the programmer collaborates with the compiler to make these proofs go through</p>
</blockquote>
<p>that's not a fundamental difference. UB is a way for the programmer to collaborate with the compiler, by offloading part of the proof burden from the compiler onto the programmer..<br>
it's somewhat crude, but the issue at hand is not caused by the crudeness of the interface, I claim.</p>



<a name="219959152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959152">(Dec 15 2020 at 10:21)</a>:</h4>
<p>well my goal is actually to create a usable language ^_^ but I appreciate that it's not the most appropriate reference for the current discussion</p>



<a name="219959218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959218">(Dec 15 2020 at 10:22)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219959152">said</a>:</p>
<blockquote>
<p>well my goal is actually to create a usable language ^_^ but I appreciate that it's not the most appropriate reference for the current discussion</p>
</blockquote>
<p>That's great, too. :-)</p>



<a name="219959226"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959226" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959226">(Dec 15 2020 at 10:22)</a>:</h4>
<p>but it's also hard</p>



<a name="219959238"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959238" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959238">(Dec 15 2020 at 10:22)</a>:</h4>
<p>there's a reason that in academia, when we try fundamentally new things, we always use toy examples</p>



<a name="219959268"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959268" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959268">(Dec 15 2020 at 10:22)</a>:</h4>
<p>you might call it "prototyping"; proper engineers do it, too ;)</p>



<a name="219959306"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959306" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959306">(Dec 15 2020 at 10:23)</a>:</h4>
<p>In my case I need the language to write a program, so I need it to be usable, but only barely and only by me</p>



<a name="219959347"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959347" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959347">(Dec 15 2020 at 10:23)</a>:</h4>
<p>hm, that seems like a goal that is orthogonal to this discussion then</p>



<a name="219959359"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959359" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959359">(Dec 15 2020 at 10:23)</a>:</h4>
<p>(which is fair, just pointing that out)</p>



<a name="219959422"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959422" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959422">(Dec 15 2020 at 10:24)</a>:</h4>
<p>well that's just to say that I am somewhere between "toy" and "production language"</p>



<a name="219959460"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959460" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959460">(Dec 15 2020 at 10:24)</a>:</h4>
<p>a minimal language also makes it much easier for the likes of me that want to figure out your key new idea -- if the new idea is "burried" in the huge amount of details that are needed to make a proper language, I need to spend a <em>lot</em> of time to read things that are just not relevant for this discussion</p>



<a name="219959508"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959508" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959508">(Dec 15 2020 at 10:25)</a>:</h4>
<p>Quite so, don't try too hard to read that spec</p>



<a name="219959533"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959533" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959533">(Dec 15 2020 at 10:25)</a>:</h4>
<p>;)</p>



<a name="219959536"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959536" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959536">(Dec 15 2020 at 10:25)</a>:</h4>
<p>That's mostly intended as evidence that this is actually somewhat worked out</p>



<a name="219959558"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959558" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959558">(Dec 15 2020 at 10:25)</a>:</h4>
<p>but it hasn't been packaged for consumption yet</p>



<a name="219959665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959665">(Dec 15 2020 at 10:26)</a>:</h4>
<p>fair :)</p>



<a name="219959969"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219959969" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219959969">(Dec 15 2020 at 10:30)</a>:</h4>
<p>this makes me wonder about what your claim really is... you said yourself above that the "way <code>p</code> was computed" matters. so in whatever level this matters, there <em>is</em> provenance. I thought your claim was that you have "the advantages of stacked borrows but without provenance", did I misunderstand?</p>



<a name="219960136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960136">(Dec 15 2020 at 10:32)</a>:</h4>
<p>The provenance information is still there, in the sense that you still have all these dereferenceable and non-aliasing predicates on things, but they exist in separate variables that are tracked alongside the real variables</p>



<a name="219960209"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960209" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960209">(Dec 15 2020 at 10:33)</a>:</h4>
<p>In a lot of ways this is basically "having provenance", because you can have variables carrying assertions about portions of memory and so on</p>



<a name="219960312"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960312" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960312">(Dec 15 2020 at 10:33)</a>:</h4>
<p>but when you go through an int-ptr cast, nothing really happens to the provenance variable alongside it, and if it can't be routed on the other end then the compiler rejects the code</p>



<a name="219960446"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960446" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960446">(Dec 15 2020 at 10:35)</a>:</h4>
<p>so what is the advantage then? In your notes I see it's all about having proofs of functional correctness built into the language -- making that usable is some kind of a holy grail of PL. ;) but for a language like Rust, that doesn't require proof of functional correctness for <em>all code</em>, what does this mean?</p>



<a name="219960451"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960451" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960451">(Dec 15 2020 at 10:35)</a>:</h4>
<p>or rather, in rust's setting when the user does something with that variable on the other end the compiler inserts an assertion op that invents a provenance for a value lacking one</p>



<a name="219960502"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960502" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960502">(Dec 15 2020 at 10:35)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219960451">said</a>:</p>
<blockquote>
<p>or rather, in rust's setting when the user does something with that variable on the other end the compiler inserts an assertion op that invents a provenance for a value lacking one</p>
</blockquote>
<p>but in general the compiler has no way to tell where "the other end" is</p>



<a name="219960521"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960521" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960521">(Dec 15 2020 at 10:35)</a>:</h4>
<p>many things can be done to the integer after it was cast from the pointer and before it is cast back</p>



<a name="219960562"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960562" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960562">(Dec 15 2020 at 10:36)</a>:</h4>
<p>it's when you use a value that the compiler has no provenance for</p>



<a name="219960580"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960580" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960580">(Dec 15 2020 at 10:36)</a>:</h4>
<p>right, so that's each int-to-ptr cast in the entire program (and potentially more)</p>



<a name="219960591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960591">(Dec 15 2020 at 10:36)</a>:</h4>
<p>and it is impossible to figure out which ptr-to-int cast this "matches up" with</p>



<a name="219960643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960643">(Dec 15 2020 at 10:37)</a>:</h4>
<p>yeah the compiler doesn't try to match them up except possibly in trivial cases</p>



<a name="219960661"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960661" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960661">(Dec 15 2020 at 10:37)</a>:</h4>
<p>Im not talking about the compiler, Im talking about the spec / abstract machine</p>



<a name="219960666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960666">(Dec 15 2020 at 10:37)</a>:</h4>
<p>in most cases it will just insert an assertion op, and the assertion op will cause the UB</p>



<a name="219960681"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960681" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960681">(Dec 15 2020 at 10:37)</a>:</h4>
<p>I dont care about the compiler^^ that's a detail that needs to follow the abstract machine rules</p>



<a name="219960780"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960780" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960780">(Dec 15 2020 at 10:38)</a>:</h4>
<p>the AM doesn't care about any of this, it simply requires that all pointer derefs are valid with one of these provenance validity tokens</p>



<a name="219960802"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960802" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960802">(Dec 15 2020 at 10:38)</a>:</h4>
<p>where does the provenance validity token come from in a ptr cast from an int?</p>



<a name="219960803"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960803" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960803">(Dec 15 2020 at 10:38)</a>:</h4>
<p>there's a reason that all formal semantics with provenance and int-ptr-casts end up having some form of "broadcast" / "loss of provenance" on a ptr-int-ptr roundtrip. You cannot avoid that without giving integers provenance.</p>



<a name="219960822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960822">(Dec 15 2020 at 10:39)</a>:</h4>
<p>so the problem is recast as an elaboration problem, where the compiler inserts assertions when it is not smart enough to figure out the reference is okay</p>



<a name="219960922"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960922" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960922">(Dec 15 2020 at 10:40)</a>:</h4>
<p>well, even with elaboration, the source language still has <em>some</em> behavior</p>



<a name="219960934"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960934" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960934">(Dec 15 2020 at 10:40)</a>:</h4>
<p>so saying "elaboration" doesn't help at all to explain how Rust behaves</p>



<a name="219960973"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960973" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960973">(Dec 15 2020 at 10:40)</a>:</h4>
<p>It is the same as how the semantics of rust are defined wrt the MIR, not the source</p>



<a name="219960978"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219960978" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219960978">(Dec 15 2020 at 10:40)</a>:</h4>
<p>also making elaboration depend on "how smart the compiler is" is extremely fragile... how can I as a user reason about the behavior of my code in such a world?</p>



<a name="219961039"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961039" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961039">(Dec 15 2020 at 10:41)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219960973">said</a>:</p>
<blockquote>
<p>It is the same as how the semantics of rust are defined wrt the MIR, not the source</p>
</blockquote>
<p>yes, but there the elaboration is structural and fairly simple. you said yours is "smart" in a magic and not-yet-specified way that somehow solves this problem. I claim that's impossible.</p>



<a name="219961083"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961083" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961083">(Dec 15 2020 at 10:42)</a>:</h4>
<p>I was waiting for that objection. :) My preference would be that the compiler never has to invent the assertions, they are all explicitly in the code, but that's a lot less backward compatible</p>



<a name="219961159"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961159" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961159">(Dec 15 2020 at 10:42)</a>:</h4>
<p>that's basically saying int-to-ptr-casts are not supported</p>



<a name="219961219"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961219" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961219">(Dec 15 2020 at 10:43)</a>:</h4>
<p>How so? I think it's closer to saying int ptr casts always lose provenance</p>



<a name="219961233"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961233" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961233">(Dec 15 2020 at 10:43)</a>:</h4>
<p>instead of having <code>int_to_ptr&lt;T&gt;(usize) -&gt; *mut T</code>, you can then only have something like <code>int_to_ptr&lt;T&gt;(addr: usize, take_provenance_from: *mut T&gt;) -&gt; *mut T</code></p>



<a name="219961338"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961338" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961338">(Dec 15 2020 at 10:44)</a>:</h4>
<p>(I know you want to split the provenance from the ptr, but "take_provenance_from" lets us talk about this without introducing syntax for the split and I think it is otherwise equivalent, only more cumbersome -- but closer to the semantics we understand better)</p>



<a name="219961340"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961340" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961340">(Dec 15 2020 at 10:44)</a>:</h4>
<p>you can have <code>int_to_ptr</code> call this assertion op, and it's UB if the assertion cannot be obtained when it is called</p>



<a name="219961400"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961400" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961400">(Dec 15 2020 at 10:45)</a>:</h4>
<p>it's UB if the compiler isn't smart enough to figure something out? uh... that seems basically unusable from a programmer perspective^^</p>



<a name="219961425"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961425" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961425">(Dec 15 2020 at 10:45)</a>:</h4>
<p>as a programemr I need clear rules to make sure my code is not UB</p>



<a name="219961434"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961434" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961434">(Dec 15 2020 at 10:45)</a>:</h4>
<p>no, I mean it's UB if at run time the proposition does not hold</p>



<a name="219961445"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961445" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961445">(Dec 15 2020 at 10:45)</a>:</h4>
<p>in the AM</p>



<a name="219961473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961473">(Dec 15 2020 at 10:45)</a>:</h4>
<p>proposition? I thought we're talking about a Rust-like language, not your "everything is verified" language?</p>



<a name="219961566"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961566" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961566">(Dec 15 2020 at 10:46)</a>:</h4>
<p>I call it an assertion because it's a property that can fail</p>



<a name="219961588"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961588" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961588">(Dec 15 2020 at 10:46)</a>:</h4>
<p>so, like <code>assume</code>?</p>



<a name="219961611"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961611" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961611">(Dec 15 2020 at 10:47)</a>:</h4>
<p>not really because this is probably not (easily) decidable</p>



<a name="219961621"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961621" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961621">(Dec 15 2020 at 10:47)</a>:</h4>
<p>if you try to take out a reference and it's already borrowed then boom</p>



<a name="219961638"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961638" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961638">(Dec 15 2020 at 10:47)</a>:</h4>
<p>undecidable UB? uh... I dont like that but let's ignore this for now^^</p>



<a name="219961659"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961659" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961659">(Dec 15 2020 at 10:47)</a>:</h4>
<p>so what does <code>int_to_ptr&lt;T&gt;(usize) -&gt; *mut T</code> elaborate to? concretely?</p>



<a name="219961671"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961671" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961671">(Dec 15 2020 at 10:47)</a>:</h4>
<p>I haven't thought carefully about it but possibly something miri-esque can get pretty close to deciding it</p>



<a name="219961826"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961826" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961826">(Dec 15 2020 at 10:49)</a>:</h4>
<div class="codehilite"><pre><span></span><code>fn int_to_ptr(x: usize) -&gt; *mut T {
  let prov = obtain_provenance_for(x);
  x as *mut T
}
</code></pre></div>
<p>oh, actually the provenance is not really needed here, my mistake</p>



<a name="219961844"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961844" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961844">(Dec 15 2020 at 10:49)</a>:</h4>
<p>this is just a cast</p>



<a name="219961899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961899">(Dec 15 2020 at 10:50)</a>:</h4>
<p>it's only when you use the pointer that a token is needed</p>



<a name="219961969"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961969" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961969">(Dec 15 2020 at 10:50)</a>:</h4>
<p>For rust, I would expect references to come bundled with a token while pointers have nothing</p>



<a name="219961990"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219961990" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219961990">(Dec 15 2020 at 10:51)</a>:</h4>
<p>which makes int-to-ptr trivial</p>



<a name="219962295"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219962295" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219962295">(Dec 15 2020 at 10:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219961638">said</a>:</p>
<blockquote>
<p>undecidable UB? uh... I dont like that but let's ignore this for now^^</p>
</blockquote>
<p>In my case I don't really care about undecidable UB because the aim is manually / semi-automatically routed proof tokens, but that's obviously a bridge too far for rust</p>



<a name="219965259"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219965259" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219965259">(Dec 15 2020 at 11:23)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219961899">said</a>:</p>
<blockquote>
<p>it's only when you use the pointer that a token is needed</p>
</blockquote>
<p>but where does the token come from, if the ptr was cast from an int? are you saying the usual code one would currently write for this in Rust is UB since I am not giving a token? That's what I mean with <code>int_to_ptr&lt;T&gt;(addr: usize, take_provenance_from: *mut T&gt;) -&gt; *mut T</code> above -- to model the intr-to-ptr cast we have currently, which <em>does</em> produce a usable pointer, we need to have a "token input" at the cast.<br>
You seem to be also adding a mostly useless token-free int-to-ptr cast; not sure what that is good for but it's not the int-to-ptr operation that Rust or C have so it shouldn't be called that.</p>



<a name="219965276"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219965276" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219965276">(Dec 15 2020 at 11:24)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219961990">said</a>:</p>
<blockquote>
<p>which makes int-to-ptr trivial</p>
</blockquote>
<p>you just shifted the exact same problem to the ptr-to-reference cast.<br>
I'd say let's assume a language which does not distinguish ptrs and references; that distinction is just a distraction.</p>



<a name="219966662"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219966662" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219966662">(Dec 15 2020 at 11:38)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219965276">said</a>:</p>
<blockquote>
<p>you just shifted the exact same problem to the ptr-to-reference cast.<br>
I'd say let's assume a language which does not distinguish ptrs and references; that distinction is just a distraction.</p>
</blockquote>
<p>That's fair, but the reason I prefer to draw the line at ptr-to-ref is because references have a rich source of lifetime information in the source, so it is much more feasible to not have to invent tokens all the time when working with them</p>



<a name="219967136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967136">(Dec 15 2020 at 11:44)</a>:</h4>
<blockquote>
<p>are you saying the usual code one would currently write for this in Rust is UB since I am not giving a token?</p>
</blockquote>
<p>For the usual rust code, the compiler would have to invent a token by inserting a <code>let prov = obtain_provenance_for(x, Raw);</code> operation, and this operation is equivalent to the effect of a read/write in SB: the compiler supplies some tag like <code>Raw</code> or <code>Uniq(other_prov)</code> containing the provenance information for this access, and this obtains the permission to read/write with the requested provenance</p>



<a name="219967482"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967482" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967482">(Dec 15 2020 at 11:49)</a>:</h4>
<p>Remark: You say to transpose everything from refs and pointers to pointers and integers, but in rust you can't write <code>ptr_to_ref</code> as a standalone function, unless the target has static lifetime or is otherwise unsound</p>



<a name="219967647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967647">(Dec 15 2020 at 11:51)</a>:</h4>
<blockquote>
<p>For the usual rust code, the compiler would have to invent a token by inserting a let prov = obtain_provenance_for(x, Raw); operation</p>
</blockquote>
<p>Stacked Borrows <em>already</em> says that the tag obtained on an int-to-ptr cast is <code>Raw</code>. But that does nothing to solve this problem.</p>



<a name="219967715"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967715" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967715">(Dec 15 2020 at 11:52)</a>:</h4>
<p>Yes, this part is not qualitatively different from SB</p>



<a name="219967718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967718">(Dec 15 2020 at 11:52)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219967482">said</a>:</p>
<blockquote>
<p>Remark: You say to transpose everything from refs and pointers to pointers and integers, but in rust you can't write <code>ptr_to_ref</code> as a standalone function, unless the target has static lifetime or is otherwise unsound</p>
</blockquote>
<p>we're concerned with UB here though, not with soundness in the "unknown safe code around us may do anything" sense</p>



<a name="219967784"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967784" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967784">(Dec 15 2020 at 11:53)</a>:</h4>
<p>Yeah, I think my model might actually conflate those (which explains why it's not likely to be decidable)</p>



<a name="219967786"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967786" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967786">(Dec 15 2020 at 11:53)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219967715">said</a>:</p>
<blockquote>
<p>Yes, this part is not qualitatively different from SB</p>
</blockquote>
<p>so if that <code>Raw</code> tag permits access to memory locations that were previously subject to a ptr-to-int cast... then you still have all the problems that the blog post points out. and if it doesn't, the cast is basically useless.</p>



<a name="219967918"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967918" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967918">(Dec 15 2020 at 11:54)</a>:</h4>
<p>It seems this is closer to a program logic for unsafe rust functions. I think you can get something with a more global sense of UB where functions are allowed to get tokens they were not passed by getting them from a global store of tokens, but that's just a fancy way of saying "provenance is in memory"</p>



<a name="219967941"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219967941" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219967941">(Dec 15 2020 at 11:54)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219967784">said</a>:</p>
<blockquote>
<p>Yeah, I think my model might actually conflate those (which explains why it's not likely to be decidable)</p>
</blockquote>
<p>Yeah I got that feeling a few times as well, but... defining <em>soundness</em> precisely is a monumental task. My thesis shows what it takes, and it is far from complete or final in that regard. And moreover, usually soundness is defined <em>in terms of a preexisting notion of UB</em>, and I dont know how to break that cycle if you now want to define UB in terms of soundness.</p>



<a name="219968171"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968171" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968171">(Dec 15 2020 at 11:57)</a>:</h4>
<p>also I'd prefer the Rust spec to not require a PhD in PL theory to understand ;)</p>



<a name="219968188"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968188" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968188">(Dec 15 2020 at 11:57)</a>:</h4>
<p>It's not a cycle here since this is just a weird undecidable definition of UB that acts more like soundness than op.sem failure, it's not saying not-UB = sound directly. It's probably also not true that not-UB = sound here, although the gap is a lot smaller than normal</p>



<a name="219968253"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968253" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968253">(Dec 15 2020 at 11:58)</a>:</h4>
<p>but of course exploring that direction could still be interesting even if it might not be the best choice for Rust :)</p>



<a name="219968298"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968298" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968298">(Dec 15 2020 at 11:58)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219968188">said</a>:</p>
<blockquote>
<p>It's not a cycle here since this is just a weird undecidable definition of UB that acts more like soundness than op.sem failure, it's not saying not-UB = sound directly. It's probably also not true that not-UB = sound here, although the gap is a lot smaller than normal</p>
</blockquote>
<p>yeah I think that's the thing I would like to see worked out in detail for a language with no more than 2 types whose grammar and op.sem fits on a napkin, so one can focus on the soundness/UB/opsem interaction without being bogged down by other details^^</p>



<a name="219968304"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968304" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968304">(Dec 15 2020 at 11:58)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219968171">said</a>:</p>
<blockquote>
<p>also I'd prefer the Rust spec to not require a PhD in PL theory to understand ;)</p>
</blockquote>
<p>That's all a matter of presentation. I think Rust itself is a good example that shows that something that only PL researchers could dream of can become part of a mainstream language</p>



<a name="219968485"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968485" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968485">(Dec 15 2020 at 12:00)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219968304">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219968171">said</a>:</p>
<blockquote>
<p>also I'd prefer the Rust spec to not require a PhD in PL theory to understand ;)</p>
</blockquote>
<p>That's all a matter of presentation. I think Rust itself is a good example that shows that something that only PL researchers could dream of can become part of a mainstream language</p>
</blockquote>
<p>FWIW, Rust went well beyond the things PL researchers dreamed off. ;) <code>&amp;mut</code>, the way Niko made it, is a key innovation in Rust that was not described in the literature before (I think).<br>
But what Rust did is make this usable without people having to understand it. The entire point about unsafe code is people have to understand the rules it follows to be able to write correct code. <em>Those rules</em> are what I say should not require a PhD.</p>



<a name="219968871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219968871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219968871">(Dec 15 2020 at 12:05)</a>:</h4>
<p>Certainly the language I'm working on is intended to be designed so that you can get by with an operational understanding of the compiler as a kind of souped up borrow checker. It is still an open problem how well random programmers will take to types that are so precise as to basically be proofs, but I am more hopeful than most in this area, having spent a lot of time teaching dependent type theory to newcomers. But this is certainly not something that I expect to slot into the rust language as it exists today.</p>



<a name="219969216"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969216" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969216">(Dec 15 2020 at 12:08)</a>:</h4>
<p>it's inspiring to see people have big dreams :)</p>



<a name="219969240"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969240" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969240">(Dec 15 2020 at 12:08)</a>:</h4>
<p>Focusing only on the question of how this could affect today's rust, I think it may turn out that all the stuff about separate provenance doesn't really matter considering the interface rust programmers are given, and the only actual novelty may be some intrinsics for producing provenances that have been erased</p>



<a name="219969293"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969293" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969293">(Dec 15 2020 at 12:09)</a>:</h4>
<p>If we have such intrinsics, then it becomes more palatable to just say that int to ptr casts are provenance erasing</p>



<a name="219969337"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969337" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969337">(Dec 15 2020 at 12:10)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219969293">said</a>:</p>
<blockquote>
<p>If we have such intrinsics, then it becomes more palatable to just say that int to ptr casts are provenance erasing</p>
</blockquote>
<p>by erasing you mean, the resulting ptr is unusable without explicitly attaching provenance to it?</p>



<a name="219969393"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969393" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969393">(Dec 15 2020 at 12:10)</a>:</h4>
<p>(so that would be the unnamed "option 4" in my post: the original program has UB)</p>



<a name="219969504"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969504" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969504">(Dec 15 2020 at 12:11)</a>:</h4>
<p>ah, you're right. If it makes the pointer invalid then we're making lots of code UB, and if the compiler inserts a validity assertion then it's being magic and the desugaring is hard to predict</p>



<a name="219969655"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969655" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969655">(Dec 15 2020 at 12:13)</a>:</h4>
<p>I suppose it's not too magical to say that source level int-to-ptr inserts a validity assertion</p>



<a name="219969759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969759">(Dec 15 2020 at 12:14)</a>:</h4>
<p>oh but the source of the provenance has to be invented too, and that probably will be too magical</p>



<a name="219969783"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969783" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969783">(Dec 15 2020 at 12:14)</a>:</h4>
<p>unless it's always <code>Raw</code> and then we have stock SB</p>



<a name="219969969"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219969969" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219969969">(Dec 15 2020 at 12:16)</a>:</h4>
<p>Okay, so revised plan: it's always <code>Raw</code> when you use <code>as *mut T</code>, but you can use another operation like <code>copy_provenance_from()</code> if you want to have a nontrivial provenance</p>



<a name="219970208"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219970208" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219970208">(Dec 15 2020 at 12:19)</a>:</h4>
<p>that might not even differ from the status quo, at least as far as rust + SB is concerned. LLVM is still miscompiling</p>



<a name="219974364"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219974364" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219974364">(Dec 15 2020 at 12:59)</a>:</h4>
<p>I have been thinking about something I wanted to do to optimize Cranelift ir after <span class="user-mention" data-user-id="271719">@Mario Carneiro</span>'s idea of using permissions rather than provenance. Let's take the example from the blog post</p>
<div class="codehilite"><pre><span></span><code>ss_p = stack_slot explicit 1
ss_q = stack_slot explicit 1
%zero = iconst.i8 0
store ss_p, %zero
store ss_q, %zero
%p = ptr2int(stack_addr ss_p)
%ip = iadd_imm %p, 1
%iq = ptr2int(stack_addr ss_q)
%eq = icmp %iq, %ip
br_false %eq, bb_end
%ten = iconst.i8 10
store int2ptr(%iq), %ten
%q_0 = stack_load.i8 ss_q
bb_end:
</code></pre></div>
<p>What if we separate the "provenance" from the pointer itself.</p>
<div class="codehilite"><pre><span></span><code>ss_p = stack_slot explicit 1
ss_q = stack_slot explicit 1
%zero = iconst.i8 0
store {ss_p} ss_p, %zero
store {ss_q} ss_q, %zero
%p = stack_addr ss_p
%ip = iadd_imm %p, 1
%iq = stack_addr ss_q
%eq = icmp %iq, %ip
br_false %eq, bb_end
%ten = iconst.i8 10
store {ss_q} iq, %ten
%q_0 = stack_load.i8 {ss_q} ss_q
bb_end:
</code></pre></div>
<p>The first optimization would then turn it into:</p>
<div class="codehilite"><pre><span></span><code>ss_p = stack_slot explicit 1
ss_q = stack_slot explicit 1
%zero = iconst.i8 0
store {ss_p} ss_p, %zero
store {ss_q} ss_q, %zero
%p = stack_addr ss_p
%ip = iadd_imm %p, 1
%iq = stack_addr ss_q
%eq = icmp %iq, %ip
br_false %eq, bb_end
%ten = iconst.i8 10
store {ss_q} ip, %ten
%q_0 = stack_load.i8 {ss_q} ss_q
bb_end:
</code></pre></div>
<p>The second optimization would have no effect as there are no integer &lt;-&gt; pointer casts in this provenance less ir.</p>
<p>The third optimization wouldn't fire as both the store and the load have the same permission.</p>
<p>This idea could be further extended by allowing more than one permission to be specified for memory operations. If any alone would allow the operation, the operation is allowed. Next up we could have permission groups that can be passed to other functions. All permission groups passed to a function are disjoint. If multiple pointers can alias, they will have to either have their permissions in the same group or specify all relevant permission groups when performing actual memory operations on them. In addition there will be a way to split a permission or permission group into multiple disjoint permissions/permission groups. This would be necessary to for example model <code>foo(&amp;mut a.0, &amp;mut a.1)</code>. Any pointers whose address is taken will have the permission necessary to use them added to a permission group reserved for globals.</p>
<p>I am curious if something like this would be capable of modeling stacked borrows.</p>



<a name="219976518"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219976518" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219976518">(Dec 15 2020 at 13:15)</a>:</h4>
<p>Yes! This is what I meant earlier. You've rewritten <code>q</code> to <code>p</code>, but <code>ss_q</code> is still there so the third optimization is blocked.</p>
<p>To support stacked borrows, you need the permissions to be essentially borrow stacks; you can create a new one by extending an existing borrow stack (which locks that one until the newly created borrow stack is dropped / goes out of scope / is invalidated by an access to the parent).</p>
<p>However, as observed above, this entails difficulties when manufacturing permissions from nothing, which happens primarily in int-to-ptr casts. To support this you have to be able to borrow from a permission you were not given, and have obtained only by reading memory at some integer location. If you have borrow stacks stored in memory in order to enable the access, you get essentially the SB model.</p>
<p>But I think this is fine; it means the only difference is that provenances are stored separately in virtual registers of the SSA, while memory still has provenance and you tuple the provenance with the address when you read or write memory.</p>



<a name="219976932"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219976932" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219976932">(Dec 15 2020 at 13:18)</a>:</h4>
<p>Int-to-ptr casts would use the globals permission group.</p>



<a name="219977191"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977191" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977191">(Dec 15 2020 at 13:20)</a>:</h4>
<blockquote>
<p>To support stacked borrows, you need the permissions to be essentially borrow stacks; you can create a new one by extending an existing borrow stack (which locks that one until the newly created borrow stack is dropped / goes out of scope / is invalidated by an access to the parent).</p>
</blockquote>
<p>That would be the way to split permission groups and merge permission groups when calling functions I talked about, right?</p>



<a name="219977272"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977272" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977272">(Dec 15 2020 at 13:20)</a>:</h4>
<p>well you want the permissions to still have an SB-like structure to support the kind of alias analysis that rust does</p>



<a name="219977323"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977323" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977323">(Dec 15 2020 at 13:21)</a>:</h4>
<p>bags of permissions would work but would not be precise enough for SB</p>



<a name="219977391"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977391" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977391">(Dec 15 2020 at 13:22)</a>:</h4>
<p>I think doing a split where you ignore one half would be equivalent to pushing an item to the borrow stack.</p>



<a name="219977473"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977473" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977473">(Dec 15 2020 at 13:22)</a>:</h4>
<p>Oh I see you mean split like a partial read permission</p>



<a name="219977648"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977648" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977648">(Dec 15 2020 at 13:24)</a>:</h4>
<p>I think that would work, although I recall the formal model in the SB paper having more bells and whistles than this so I might be forgetting something</p>



<a name="219977719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977719">(Dec 15 2020 at 13:24)</a>:</h4>
<p>A split would take one permission group and create multiple new ones. You could say that certain permission groups only allow read access, while others allow both read and write access.</p>



<a name="219977974"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/219977974" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#219977974">(Dec 15 2020 at 13:27)</a>:</h4>
<p>These should basically follow the same rules as the separation logic assertions in the SB paper</p>



<a name="220091949"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220091949" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220091949">(Dec 16 2020 at 09:11)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/219977974">said</a>:</p>
<blockquote>
<p>These should basically follow the same rules as the separation logic assertions in the SB paper</p>
</blockquote>
<p>there are no separation logic assertions in the SB paper?</p>



<a name="220092041"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220092041" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220092041">(Dec 16 2020 at 09:12)</a>:</h4>
<blockquote>
<p>What if we separate the "provenance" from the pointer itself.</p>
</blockquote>
<p>The tricky bit is figuring out the <code>ss_q</code> in the <code>store {ss_q} iq</code>, isn't it? in general you have no idea where that integer is coming from.<br>
If you have a "wildcard" group, then I don't see how this makes anything any easier than implicitly adding the wildcard like current compilers do.</p>



<a name="220094629"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220094629" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220094629">(Dec 16 2020 at 09:41)</a>:</h4>
<p><code>ss_q</code> here is a permission that allows access to just the stack slot containing <code>q</code>.</p>



<a name="220094719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220094719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220094719">(Dec 16 2020 at 09:42)</a>:</h4>
<p>In the general case getting the permissions could be done by taking an ir that does have provenance and then elaborating it to this permission based model.</p>



<a name="220095117"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220095117" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220095117">(Dec 16 2020 at 09:47)</a>:</h4>
<p>Oops, I meant the rustbelt paper, specifically the lifetime rules on p.23 of <a href="https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf">https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf</a></p>



<a name="220115667"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220115667" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220115667">(Dec 16 2020 at 13:38)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220095117">said</a>:</p>
<blockquote>
<p>Oops, I meant the rustbelt paper, specifically the lifetime rules on p.23 of <a href="https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf">https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf</a></p>
</blockquote>
<p>those rules are for references only. raw pointers probably need to be much less restricted than that.</p>



<a name="220115765"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220115765" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220115765">(Dec 16 2020 at 13:39)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220094629">said</a>:</p>
<blockquote>
<p><code>ss_q</code> here is a permission that allows access to just the stack slot containing <code>q</code>.</p>
</blockquote>
<p>FWIW, I think "permission" and "provenance" are entirely synonynmous at this point... or at least if there is a distinction I dont see it.^^ your main point seems to be about adding some APIs that treat provenance more explicitly, but that could be easily added to any provenance model I think.</p>



<a name="220116279"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220116279" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220116279">(Dec 16 2020 at 13:44)</a>:</h4>
<p>The thing I dont understand is which problem this solves / what the goal here is.</p>
<p>Colleagues of mine are working on C verification and they have a language where int-to-ptr cast works different: you need to also provide a pointer from which the provenance is taken. That's along the lines of what I proposed above when I tried to understand <span class="user-mention" data-user-id="271719">@Mario Carneiro</span>'s approach. This makes int-to-ptr casts <em>strictly weaker</em> (there is no way to lower Rust or LLVM IR into this), and the benefit they get for paying this price is that there is no need to "guess" a provenance when casting an int back to a ptr, and there is no such thing as a ptr-int-ptr roundtrip (because there is no operation of type <code>int -&gt; ptr</code>) that could be handled incorrectly.</p>
<p>But you said you can lower Rust/MIR/LLVM IR to your proposal, so this must be something different. My guess is that it helps against "forgetting that provenance exists" by making provenance more explicit, but doesn't actually make precisely defining the behvavior of int-to-ptr casts any easier?</p>



<a name="220116374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220116374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220116374">(Dec 16 2020 at 13:45)</a>:</h4>
<p>Basically, I am asking, what does LLVM's <code>inttoptr</code> (or the MIR equivalent) lower to in your proposal?</p>



<a name="220116777"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220116777" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220116777">(Dec 16 2020 at 13:49)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220115667">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220095117">said</a>:</p>
<blockquote>
<p>Oops, I meant the rustbelt paper, specifically the lifetime rules on p.23 of <a href="https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf">https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf</a></p>
</blockquote>
<p>those rules are for references only. raw pointers probably need to be much less restricted than that.</p>
</blockquote>
<p>Well, as I mentioned at the start, I prefer to draw the line at ptr-to-ref for exactly this reason. The rules for ptr-to-int are trivial. Sure, we wouldn't be able to do that in C, but I'm not talking about C.</p>



<a name="220117063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220117063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220117063">(Dec 16 2020 at 13:51)</a>:</h4>
<p>I agree that getting a sane provenance system for C is very difficult exactly because the annotations are basically absent, so the compiler and the semantics have to invent all the borrowing structure without any information, and so you get these crazy nondeterministic uncheckable rules.</p>



<a name="220117073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220117073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220117073">(Dec 16 2020 at 13:51)</a>:</h4>
<p>The difference between provenance and the proposed permissions is that provenance is attached to pointers themself while permissions are attached to memory operations.</p>



<a name="220117618"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220117618" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220117618">(Dec 16 2020 at 13:56)</a>:</h4>
<blockquote>
<p>But you said you can lower Rust/MIR/LLVM IR to your proposal, so this must be something different. My guess is that it helps against "forgetting that provenance exists" by making provenance more explicit, but doesn't actually make precisely defining the behvavior of int-to-ptr casts any easier?</p>
</blockquote>
<p>While I have come around to the view that they aren't as different as I thought originally, I believe that there is an advantage for IRs to keep them separate because it makes it easier to perform transformations on the two parts separately, and avoid errors like GVN that think that the provenance is a function of the bit pattern, which we know is false. It's possible to retrofit this into an IR that assumes that pointer values have provenance baked in, as long as you have a <code>copy_provenance</code> operation, so perhaps that's a better path forward for things like LLVM, but I personally find it a lot easier not to fall into erroneous thinking when you keep them separate.</p>



<a name="220118617"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220118617" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220118617">(Dec 16 2020 at 14:03)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220116374">said</a>:</p>
<blockquote>
<p>Basically, I am asking, what does LLVM's <code>inttoptr</code> (or the MIR equivalent) lower to in your proposal?</p>
</blockquote>
<p>Regarding LLVM's <code>inttoptr</code> operation, assuming LLVM style pointer provenance, it depends on whether integers also have provenance. In the provenance language, if ints have provenance then inttoptr just keeps that provenance, and if they don't then it creates a wildcard provenance; in the permissions language then the cast is just a bit pattern cast and we use the permission associated to the int (if ints have provenance and this one has a permission), otherwise we invent a wildcard permission. (There isn't anything fundamentally different between the models here.)</p>



<a name="220118967"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220118967" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220118967">(Dec 16 2020 at 14:06)</a>:</h4>
<p>Actually I guess there is a difference if we only invent the permission at first use rather than when we create the pointer in the first place; I'm not sure what the C rules say about when the UB is actually triggered.</p>



<a name="220127987"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220127987" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220127987">(Dec 16 2020 at 15:16)</a>:</h4>
<p>Permissions are more flexible than provenance. With provenance you have to determine in advance when creating an ir what has and doesn't have provenance, while with permissions the frontend is free to choose whatever permissions it wants. Functions that don't read or write any external memory are easily modeled as functions that don't accept any permissions rather than as a special attribute. For WASM it would also be possible to only give the WASM access to the linear memory and nothing else, not even pointers that had a ptr2int operation on them by only passing a single permission for the linear memory and no other permissions.</p>



<a name="220129420"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220129420" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220129420">(Dec 16 2020 at 15:27)</a>:</h4>
<p>I think the big question is what to do about "invented" permissions. These are necessary to model ptr2int operations in a LLVM compatible way, but they are basically unsound if you take a strict approach to permissions. It's possible to do quite a lot without them, e.g. replacing int2ptr with <code>copy_provenance</code> as Ralf mentioned, and possibly this is sufficient for WASM, but assuming that these are needed and should not always be trivially UB, you need some story for how to borrow permission from a variable in another stack frame or even another thread without an actual data dependency.</p>



<a name="220129694"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220129694" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220129694">(Dec 16 2020 at 15:29)</a>:</h4>
<p>Borrowing a permission from a parent stack frame is a matter of passing the permission to the function. Borrowing a permission from a child stack frame would not be allowed as all stack allocations are deallocated. Borrowing from another thread is a good question how to do.</p>



<a name="220129802"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220129802" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220129802">(Dec 16 2020 at 15:30)</a>:</h4>
<p>the problem is that those all require explicit data dependencies, and essentially a modification of the code</p>



<a name="220129894"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220129894" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220129894">(Dec 16 2020 at 15:31)</a>:</h4>
<p>in other words, it's totally possible for a language to be built like this and be pretty expressive, but if you want to capture "in the wild" C/Rust/LLVM code this won't cut it</p>



<a name="220130366"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220130366" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220130366">(Dec 16 2020 at 15:34)</a>:</h4>
<p>This example <a href="https://github.com/rust-lang/unsafe-code-guidelines/issues/263">https://github.com/rust-lang/unsafe-code-guidelines/issues/263</a> shows raw pointers being used to enable "action at a distance", where the permission in the parent is never passed to the child but it obtains the permission anyway via raw pointers</p>



<a name="220409793"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220409793" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220409793">(Dec 18 2020 at 18:20)</a>:</h4>
<blockquote>
<p>It's possible to retrofit this into an IR that assumes that pointer values have provenance baked in</p>
</blockquote>
<p>It's not just about the IRs. <em>Surface Rust</em> has provenance baked in, so any IR that wants to do something different needs to work quite a bit to get there.</p>



<a name="220409882"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220409882" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220409882">(Dec 18 2020 at 18:21)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220117073">said</a>:</p>
<blockquote>
<p>The difference between provenance and the proposed permissions is that provenance is attached to pointers themself while permissions are attached to memory operations.</p>
</blockquote>
<p>I don't know what you mean by this... <em>the entire point</em> of provenance is that we need something that's attached to the value. That's what makes the aliasing rules work.</p>



<a name="220410135"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410135" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410135">(Dec 18 2020 at 18:23)</a>:</h4>
<p><span class="user-mention" data-user-id="271719">@Mario Carneiro</span> </p>
<blockquote>
<p>in the permissions language then the cast is just a bit pattern cast and we use the permission associated to the int (if ints have provenance and this one has a permission), otherwise we invent a wildcard permission. (There isn't anything fundamentally different between the models here.)</p>
</blockquote>
<p>that makes sense and reaffirms my believe that they are equivalent. "permissions" are just slightly desugaring some of the things that are implicit in provenance. which can be very helpful to avoid mistakes, but does not fundamentally make the problem any easier. it's just a potentially better API to the same thing.</p>



<a name="220410241"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410241" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410241">(Dec 18 2020 at 18:24)</a>:</h4>
<p>With provenance you have the value of a pointer and the provenance bundled together. The idea with permissions is that you split both, so you can optimize the pointers as if they are integers, but memory operations take a permission as a separate input from the integer value of the pointer.</p>



<a name="220410301"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410301" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410301">(Dec 18 2020 at 18:25)</a>:</h4>
<p><span class="user-mention" data-user-id="133247">@bjorn3</span> seems to think of something else entirely and I am entirely lost there.</p>
<blockquote>
<p>With provenance you have to determine in advance when creating an ir what has and doesn't have provenance, while with permissions the frontend is free to choose whatever permissions it wants. </p>
</blockquote>
<p>?!? The set of possible permissions needs to be defined up-front when the IR is defined, how does this have anything to do with provenance? How would Miri check "permissions" if they are not fixed as part of the IR? I am totally lost.</p>



<a name="220410344"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410344" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410344">(Dec 18 2020 at 18:25)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220410241">said</a>:</p>
<blockquote>
<p>With provenance you have the value of a pointer and the provenance bundled together. The idea with permissions is that you split both, so you can optimize the pointers as if they are integers, but memory operations take a permission as a separate input from the integer value of the pointer.</p>
</blockquote>
<p>well but you need to model a language (Rust) where the permissions associated with a pointer are carried along with the pointer value</p>



<a name="220410419"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410419" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410419">(Dec 18 2020 at 18:26)</a>:</h4>
<p>so is this any different than just replacing <code>ptr</code> by <code>(address, provenance)</code> as part of the lowering?</p>



<a name="220410452"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410452" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410452">(Dec 18 2020 at 18:26)</a>:</h4>
<p>The lowering is just that, yes</p>



<a name="220410466"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410466" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410466">(Dec 18 2020 at 18:27)</a>:</h4>
<p>but during optimization the two will diverge more</p>



<a name="220410545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410545">(Dec 18 2020 at 18:27)</a>:</h4>
<p>that sounds like an interesting experiment, but it is pretty much exactly what formal models of provenance already do</p>



<a name="220410557"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410557" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410557">(Dec 18 2020 at 18:27)</a>:</h4>
<p>just more explicitly exposed on the IR level</p>



<a name="220410647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410647">(Dec 18 2020 at 18:28)</a>:</h4>
<p>so, there's no fundamental difference then. just a more explicit account of provenance. I'm all for that, I am just confused by the claims that this would somehow make any problems go away.^^</p>



<a name="220410749"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410749" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410749">(Dec 18 2020 at 18:29)</a>:</h4>
<p>I think that a strategy such as the one I'm taking in my language can actually make the problems go away, but that solution is most likely not applicable to rust</p>



<a name="220410762"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410762" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> bjorn3 <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410762">(Dec 18 2020 at 18:29)</a>:</h4>
<p>Because provenance and pointer addresses are no longer bundled together in the ir, it becomes valid to optimize the pointer address in ways that would normally be invalid because of differing provenance.</p>



<a name="220410814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410814">(Dec 18 2020 at 18:30)</a>:</h4>
<p>maybe what <span class="user-mention" data-user-id="133247">@bjorn3</span> meant above by "not having to determine things in advance" is that many places don't care what exactly the structure of the <code>provenance</code> component is? the same is true in provenance models, though. and some optimizations <em>do</em> care so you still need to fix it when precisely spec'in an IR.</p>



<a name="220410920"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410920" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410920">(Dec 18 2020 at 18:30)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220410749">said</a>:</p>
<blockquote>
<p>I think that a strategy such as the one I'm taking in my language can actually make the problems go away, but that solution is most likely not applicable to rust</p>
</blockquote>
<p>if you push this explicit view of provenance all the way to the user, then maybe you can avoid even having a wildcard provenance. is that the point? I'd agree with that.</p>



<a name="220410945"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410945" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410945">(Dec 18 2020 at 18:30)</a>:</h4>
<p>yes, that's the idea</p>



<a name="220410990"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410990" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410990">(Dec 18 2020 at 18:31)</a>:</h4>
<p><span class="user-mention silent" data-user-id="271719">Mario Carneiro</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220410945">said</a>:</p>
<blockquote>
<p>yes, that's the idea</p>
</blockquote>
<p>as I mentioned, that's eactly what some colleagues are doing for C verification</p>



<a name="220410993"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220410993" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220410993">(Dec 18 2020 at 18:31)</a>:</h4>
<p>you allow the user to actually validate int-ptr casts</p>



<a name="220411022"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220411022" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220411022">(Dec 18 2020 at 18:31)</a>:</h4>
<p>the engineers agreed it is okay to have to annotate provenance on int-to-ptr casts</p>



<a name="220411059"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220411059" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220411059">(Dec 18 2020 at 18:31)</a>:</h4>
<p>I am confused by the term "validate" here, do you mean anything else than "explicitly indicating the provenance"?</p>



<a name="220411149"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220411149" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220411149">(Dec 18 2020 at 18:32)</a>:</h4>
<p>I often get the sentiment from C programmers that they don't <em>like</em> that the compiler is making all these assumptions and want to be more explicit about things. I'm sure I'm giving them far more than they asked for though :)</p>



<a name="220411165"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220411165" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220411165">(Dec 18 2020 at 18:32)</a>:</h4>
<p>oh right it's because of your built-in logic? you don't even have to go there for such a model though. you can do this in C, just remove int-to-ptr casts and replace them by a different API.</p>



<a name="220411275"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can%20we%20do%20without%20provenance%3F/near/220411275" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/136281-t-lang/wg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F.html#220411275">(Dec 18 2020 at 18:33)</a>:</h4>
<p><span class="user-mention silent" data-user-id="133247">bjorn3</span> <a href="#narrow/stream/136281-t-lang.2Fwg-unsafe-code-guidelines/topic/Can.20we.20do.20without.20provenance.3F/near/220410762">said</a>:</p>
<blockquote>
<p>Because provenance and pointer addresses are no longer bundled together in the ir, it becomes valid to optimize the pointer address in ways that would normally be invalid because of differing provenance.</p>
</blockquote>
<p>Okay, I see. the "end points" of the trade-offs don't change (the optimizations from my blog post still behave the same way), but it becomes possible to explore more of the "middle-ground" with this extra flexibility/expressiveness and that could be useful.</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>